T:Type, eq:EqDecider(T), es:ES, x:Id, e, e':E.
@loc(e')(x:T)
 (e <loc e')
 (((x after e) = (x when e')  T)  ((x after lastchange(x;e')) = (x when e')  T)) 

latex

Definitions	{T}, P  Q, P  Q, P & Q, , t  T, P  Q, P  Q, EqDecider(T), x:A. B(x), (e <loc e'), @i(x:T)
Lemmas	es-when wf, es-after-lc-before, assert wf, iff wf, bool wf, event system wf, Id wf, es-E wf, es-locl wf, es-vartype wf, es-loc-lc, es-loc wf, es-dtype wf, es-lc wf, es-after wf, es-lc-cases